$\forall$${\it es}$:ES, $l_{1}$, $l_{2}$:IdLnk, ${\it tg}$:Id, $A$:Type.
\\[0ex]links2Fifo{-}impl(${\it es}$;$l_{1}$;$l_{2}$;$A$;${\it tg}$)
\\[0ex]$\in$ ($A$:Type $\times$ ($B$:Type $\times$ $C$:Type $\times$ $S$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$) $\times$ $R$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$) $\times$ (:($C$$\rightarrow$$A$$\rightarrow$$B$$\rightarrow\mathbb{P}$) $\times$ Top)))